Search for: All records

We analyze the Secure Remote Password (SRP) protocol for structural weaknesses using the Cryptographic Protocol Shapes Analyzer (CPSA) in the first formal analysis of SRP (specifically, Version 3). SRP is a widely deployed Password Authenticated Key Exchange (PAKE) protocol used in 1Password, iCloud Keychain, and other products. As with many PAKE protocols, two participants use knowledge of a preshared password to authenticate each other and establish a session key. SRP aims to resist dictionary attacks, not store plaintext-equivalent passwords on the server, avoid patent infringement, and avoid export controls by not using encryption. Formal analysis of SRP is challenging in part because existing tools provide no simple way to reason about its use of the mathematical expression “v + g b mod q”. Modeling v + g b as encryption, we complete an exhaustive study of all possible execution sequences of SRP. Ignoring possible algebraic attacks, this analysis detects no major structural weakness, and in particular no leakage of any secrets. We do uncover one notable weakness of SRP, which follows from its design constraints. It is possible for a malicious server to fake an authentication session with a client, without the client’s participation. This action might facilitate an escalation of privilege attack, if the client has higher privileges than does the server. We conceived of this attack before we used CPSA and confirmed it by generating corresponding execution shapes using CPSA. 

Locating arrays are designs used in combinatorial testing with the property that every set of d t-way interactions appears in a unique set of tests. Using a locating array to conduct fault testing ensures that faulty interactions can be located when there are d or fewer faults. Locating arrays are fairly new and few techniques have been explored for their construction. Most of the available work is limited to finding only one fault. Known general methods require a covering array of strength t+d and produce many more tests than are needed. We present Partitioned Search with Column Resampling (PSCR), a randomized computational search algorithmic framework to verify if an array is (d t)-locating by partitioning the search space to decrease the number of comparisons. If a candidate array is not locating, random resampling is performed until a locating array is constructed or an iteration limit is reached. Results are compared against known locating array constructions from covering arrays of higher strength and against published results of mixed level locating arrays for parameters of real-world systems. The use of PSCR to build larger locating arrays from a variety of ingredient arrays is explored.